home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / interp_2.06.0 < prev    next >
Text File  |  1992-04-03  |  19KB  |  674 lines
  1. %%% INTERPRETER
  2. %%% version 2.00.0 (based on interp_19.1)
  3. %%%   added equality transformation
  4. %%% version 2.00.1
  5. %%%   added equality rewriting
  6. %%% version 2.00.4
  7. %%%   fixed input clause count when transforming equation
  8. %%% version 2.00.6
  9. %%%   added user specified rewrite rules and orderings
  10. %%%   added "include_original_clause"
  11. %%% version 2.01.1
  12. %%%   fixed transivity bug when asserting rewrite order
  13. %%% version 2.01.3
  14. %%%   moved rewriting of input clauses to interpret
  15. %%%   added code to orient equations
  16. %%% version 2.01.4
  17. %%%   modified rewriting of equations according to David Plaisted's method
  18. %%% version 2.01.7
  19. %%%   oriented input equations literal in each direction
  20. %%% version 2.01.9
  21. %%%   optimized term rewriting
  22. %%% version 2.02.1
  23. %%%   added partial rewrite count
  24. %%% version 2.03.0
  25. %%%   moved rewrite rule simplification to hyper-linking
  26. %%% version 2.03.4
  27. %%%   printed axioms
  28. %%% version 2.03.8
  29. %%%   rewrite clauses in round 0 when necessary
  30. %%% version 2.04.5
  31. %%%   don't include original equations in both directions
  32. %%% version 2.05.1
  33. %%%   added clause splitting
  34. %%% version 2.05.3
  35. %%%   added support for Quintus Prolog
  36. %%% version 2.05.4
  37. %%%   don't assert duplicate input clauses including pulled out forms
  38. %%% version 2.05.8
  39. %%%   renamed assign/2 to assign_cmd/2 for compatibility with Quintus Prolog 3
  40. %%%   added priority_bound_increment
  41. %%% version 2.06.0
  42. %%%   added bug fixes from Shie-Jue
  43. %%%
  44. %%% This is an interpreter to 
  45. %%%     1. read the input clauses
  46. %%%    2. transform the input clauses into internal clause format
  47. %%%    3. read in the commaneds in the input file and execute them
  48. %%%    4. set supported information for clauses
  49. %%%    5. Initialize distances
  50. %%%
  51. %%% Interp fails in the following cases:
  52. %%%     Read erroneous commands
  53. %%%    No user support clauses if user support strategy is specified.
  54. %%%
  55. %%% For axioms:
  56. %%%    axiom_list(sprfn|clause)
  57. %%% For replace rules:
  58. %%%    replace_list
  59. %%% For weights:
  60. %%%    weight_list
  61. %%% For set of support:
  62. %%%    set_of_support.
  63. %%%    
  64. %%% There are 6 errors that make this procedure fail.
  65. %%%    too_many_input_variables
  66. %%%    no_unit_clauses_with_oorr_support
  67. %%%    no_user_clauses_with_uorn_support
  68. %%%    no_neg_clauses_with_n_support
  69. %%%    error in user_rewrite section
  70. %%%    format_error_input_file
  71. %%%
  72. %%% Separate replace rules into two sets.
  73. %%%        repeated_replace_rules.
  74. %%%        rules.
  75. %%%        end.
  76. %%%        once_replace_rules.
  77. %%%        rules.
  78. %%%        end.
  79. %%%
  80. %%% Add context literals.
  81. %%%    The input replace rule is C,F,X.
  82. %%%
  83.  
  84.      interp :- not(not(interp_fail)).
  85.  
  86.      interp_fail :-
  87.     cputime(TT1),
  88.     file_name(File),
  89.     seeing(Input),
  90.     see(File), !,
  91.     abolish(neg_clause_with_n_support,0),
  92.     !, interp_0(Input),
  93.     seen,
  94.     see(Input),
  95.     cputime(TT2),
  96.     TT3 is TT2 - TT1,
  97.     nl,
  98.     write_line(5,'interp(s): ',TT3), !.
  99.  
  100.      interp_0(Input) :-
  101.     interp_1, !.
  102. %%% If interp fail abnormally, close the file and return to the 
  103. %%%    original input stream.
  104.      interp_0(Input) :-
  105.     seen,
  106.     see(Input), !, fail.
  107.  
  108. %%% Read until end_of_input.
  109.      interp_1 :-
  110.     read(Term),
  111.     Term \== end_of_input, !,
  112.     interp_1(Term), !,
  113.     interp_1.
  114. %%% Provide support information.
  115.      interp_1 :-
  116.     set_priority_bound_increment_default,
  117.     process_supportset,
  118.     split_clauses.
  119.  
  120. %%% Call different procedures according to the input commands.
  121.      interp_1(axiom_list(Type)) :-
  122.     !, read_axioms(0,Type), !.
  123.      interp_1(weight_list) :-
  124.     !, interp_1_weight, !.
  125.      interp_1(repeated_replace_rules(X)) :-
  126.     !, interp_1_replace(X,u), !.
  127.      interp_1(once_replace_rules(X)) :-
  128.     !, interp_1_replace(X,o), !.
  129.      interp_1(set_of_support) :-
  130.     !, read_usersupportset.
  131.      interp_1(user_rewrite) :-
  132.     !, read_userrewrite.
  133.      interp_1(set(X)) :-
  134.          !, interp_1_command(set(X)), !.
  135.      interp_1(clear(X)) :-
  136.     !, interp_1_command(clear(X)), !.
  137.      interp_1(assign(X,V)) :-
  138.     !, interp_1_command(assign_cmd(X,V)), !.
  139.      interp_1(delete(X,V)) :-
  140.     !, interp_1_command(delete(X,V)), !.
  141.      interp_1(Term) :-
  142.     assert_print_error('Syntactic error in input file !'), !, fail.
  143.  
  144. %%% Ignore weight settings if not user control.
  145.      interp_1_weight :-
  146.     user_control, !,
  147.     read_weights, !.
  148.      interp_1_weight :-
  149.         read_till_end.
  150.  
  151. %%% Ignore replace settings if not user control.
  152.      interp_1_replace(X,T) :-
  153.     user_control, !,
  154.     read_replaces(X,T), !.
  155.      interp_1_replace(_,_) :-
  156.         read_till_end.
  157.  
  158. %%% read till end command.
  159.      read_till_end :-
  160.         read(X),
  161.         X \== end,
  162.     !, read_till_end.
  163.      read_till_end.
  164.  
  165. %%% Ignore commands if not user control.
  166.      interp_1_command(X) :-
  167.     user_control, !,
  168.     X, !.
  169.      interp_1_command(_).
  170.  
  171. %%% Read in input clauses.
  172.      read_axioms(N,Type) :-
  173.     read(Term),
  174.     !, read_axioms_1(Term,N,Type).
  175.  
  176. %%% Read in axioms one by one and transforms them into semi-internal form.
  177.      read_axioms_1(end,N,_) :-
  178.         assert_eq_axioms(N,N1),
  179.     assert(number_inclauses(N1)), !.
  180.      read_axioms_1(Term,N1,Type) :-
  181.     clause_format(Type,Term,Clause1), !,
  182.     not(not(read_axioms_2(Clause1))),
  183.         assert_original_clause(Clause1,N1,N3),
  184.         eq_trans(Clause1,Clause2),
  185.         generate_rewrite_rule(Clause1,_),
  186.     semi_internal_form(Clause2,C2),
  187.     assert_semi_internal_form(C2),
  188.     N2 is N3 + 1, !,
  189.     read_axioms(N2,Type).
  190.      read_axioms_2(C) :-
  191.     vars_tail(C,V),
  192.     var_list(V),
  193.     write_line(5,'axiom:'),
  194.     write_line(10,C),
  195.     !.
  196.  
  197. %%%
  198. %%% Assert_original_clause asserts the original equation.
  199. %%%
  200.      assert_original_clause(C,N1,N2) :-
  201.         equality_transform,
  202.     include_original_clause,
  203.     !,
  204.     orient_equation(C,C1),
  205.     semi_internal_form(C1,C2),
  206.     assert_semi_internal_form(C2),
  207.     N2 is N1+1,
  208.     !.
  209.      assert_original_clause(_,N,N).
  210.  
  211. %%% Transform an input formula into clause form.
  212.      clause_format(clause,P,P) :-
  213.     is_list(P), !.
  214.      clause_format(sprfn,Line,P) :-
  215.     \+ is_list(Line),
  216.     sprfn_to_clause(Line,P), !.
  217.      clause_format(_,_,_) :-
  218.     assert_print_error('Syntactic error in input file !'), !, fail.
  219.  
  220. %%% Transform a clause into a semi-internal form.
  221. %%% If the number of variables in an input clause is greater than 
  222. %%%     the number of constants in a specified list, then fail.
  223.      semi_internal_form(Clause,cl(CV1,CSize1,
  224.         by(Cn1,V11,V12,V1,W1))) :-
  225.     linearize_term(Clause,Cn1,V11,V12),
  226.     vars_tail(Clause,V1),
  227.     !,
  228.     check_input_numbervars(V1),
  229.     clause_size(Clause,CSize1),
  230.     vars_literals(Clause,W1),
  231.     compute_V_lits(W1,0,CV1).
  232.  
  233.      check_input_numbervars(V1) :-
  234.          check_numbervars(V1,'Number of variables overflows in input clauses !'), !.
  235.      check_input_numbervars(V1) :-
  236.     assert_print_error('too_many_input_variables'), !, fail.
  237.  
  238. %%% Assert clause in semi internal form checking for duplicates.
  239.      assert_semi_internal_form(cl(_,CSize1,by(Cn1,V11,V11,V,_))) :-
  240.     not(not(assert_semi_internal_form_1(CSize,Cn1,V))),
  241.     !.
  242.      assert_semi_internal_form(C) :-
  243.     assertz(sent_C(C)),
  244.     !.
  245.      assert_semi_internal_form_1(CSize1,Cn1,V) :-
  246.     const_list(V),
  247.     sent_C(cl(_,CSize1,by(Cn1,V11,V11,V,_))),
  248.     !.
  249.  
  250. %%% Compute a list of variables for each literal.
  251.      vars_literals([L|Ls],[W|Ws]) :-
  252.     vars_tail(L,W), !,
  253.     vars_literals(Ls,Ws).
  254.      vars_literals([],[]).
  255.  
  256. %%% Read in weights and assert into database.
  257.      read_weights :-
  258.     read(Term),
  259.     read_weights_1(Term).
  260.  
  261.      read_weights_1(end) :- !.
  262.      read_weights_1((Type,Term,W)) :-
  263.     L =.. [Type,Term,W],
  264.     assertz(L), !,
  265.     read_weights.
  266.  
  267. %%% Read in replace rules and assert into database.
  268.      read_replaces(X,T) :-
  269.     read(Term), !,
  270.     read_replaces_1(Term,X,T).
  271.  
  272.      read_replaces_1(end,_,_) :- !.
  273.      read_replaces_1((C,F,X),Type,T12) :-
  274.     read_replaces_1_2(C,F,X,Type,T12),
  275.     !, read_replaces(Type,T12).
  276.      read_replaces_1((C,F),Type,T12) :-
  277.     read_replaces_1_2(C,F,[],Type,T12),
  278.     !, read_replaces(Type,T12).
  279.  
  280.      read_replaces_1_2(C,F,X,Type,T12) :-
  281.     clause_format(Type,C,Clause), !,
  282.     vars_tail(Clause,V1),
  283.     !,
  284.     check_input_numbervars(V1),
  285.     vars_literals(Clause,W1),
  286.     list_multi_Ns(Clause,0,F,1,Flags),
  287.     list_multi_Ns(Clause,0,X,1,Contexts),
  288.     read_replaces_1_1(T12,Clause,V1,W1,Flags,Contexts).
  289.  
  290.      read_replaces_1_1(u,Clause,V1,W1,Flags,Contexts) :-
  291.     assertz(replace_rule_1(Clause,V1,W1,Flags,Contexts)), !.
  292.      read_replaces_1_1(o,Clause,V1,W1,Flags,Contexts) :-
  293.     assertz(replace_rule_2(Clause,V1,W1,Flags,Contexts)), !.
  294.  
  295. %%% 1. Read in user support sets.
  296. %%% 2. delete any duplicates.
  297. %%% 3. sort the list.
  298. %%% 4. renumber support set if equality_transform and include_original_clause
  299. %%% 4. assert it into database.
  300.      read_usersupportset :-
  301.     read_usersupportset(S1),
  302.     delete_all_duplicates(S1,S2),
  303.     sort(S2,S3),
  304.     renumber_supportset(S3,S4),
  305.     assert(user_supportset(S4)).
  306.  
  307.      read_usersupportset(U) :-
  308.     read(N), !,
  309.     read_usersupportset_1(N,U).
  310.  
  311.      read_usersupportset_1(end,[]) :- !.
  312.      read_usersupportset_1(N1,[N1|U]) :-
  313.          read_usersupportset(U).
  314.  
  315.      renumber_supportset(S1,S2) :-
  316.     equality_transform,
  317.     include_original_clause,
  318.     !,
  319.     renumber_supportset_1(S1,S2).
  320.      renumber_supportset(S,S).
  321.  
  322.      renumber_supportset_1([],[]).
  323.      renumber_supportset_1([N1|S1],[N2,N3|S2]) :-
  324.        N3 is N1*2,
  325.        N2 is N3-1,
  326.        !,
  327.        renumber_supportset_1(S1,S2).
  328.  
  329. %%% Process support strategies and provide support informations.
  330.      process_supportset :-
  331.     support_list(User),
  332.     check_supplist(User),
  333.     !,
  334.     support_info.
  335.  
  336. %%% Transform user defined support specs into internal support form.
  337.      check_supplist(User) :-
  338.     name_list(User,Name),
  339.     legal_supplist(Name),
  340.     transf_supplist(Name,Int),
  341.     abolish(support_list_internal,1),
  342.     assert(support_list_internal(Int)), !.
  343.      check_supplist(User) :-
  344.     assert_print_error('Syntactic error in input file !'), !, fail.
  345.     
  346. %%% Transform an atom to a list of integers.
  347.      name_list([U|Us],[N|Ns]) :-
  348.     name(U,N), !,
  349.     name_list(Us,Ns).
  350.      name_list([],[]).
  351.  
  352. %%% Check if the support strategies specified are legal.
  353.      legal_supplist([N|Ns]) :-
  354.     legal_suppitem(N), !,
  355.     legal_supplist(Ns).
  356.      legal_supplist([]).
  357.  
  358.      legal_suppitem([T|Ts]) :-
  359.     content_suppvalue([T]), !,
  360.     legal_suppitem(Ts).
  361.      legal_suppitem([]).
  362.  
  363. %%% Specify legal support strategies.
  364.      content_suppvalue("u").
  365.      content_suppvalue("b").
  366.      content_suppvalue("f").
  367.      content_suppvalue("r").
  368.      content_suppvalue("n").
  369.      content_suppvalue("o").
  370.  
  371.      transf_supplist([N|Ns],[sup(U,B,F,R)|Is]) :-
  372.     transf_suppitem(N,U,B,F,R), !,
  373.     transf_supplist(Ns,Is).
  374.      transf_supplist([],[]).
  375.  
  376.      transf_suppitem([N|Ns],U,B,F,R) :-
  377.     transf_suppvalue([N],U,B,F,R), !,
  378.          transf_suppitem(Ns,U,B,F,R).
  379. %%% If a support is not specified, set it 0.
  380.      transf_suppitem([],U,B,F,R) :-
  381.     var_then_N(U,0),
  382.     var_then_N(B,0),
  383.     var_then_N(F,0),
  384.     var_then_N(R,0).
  385.  
  386. %%% If user support, specify what kind of user support.
  387. %%% This information is provided for supervsior to decide the completeness
  388. %%%    of a support strategy.
  389.      transf_suppvalue("u",1,B,F,R) :- assert_once(user_support(u)).
  390.      transf_suppvalue("n",1,B,F,R) :- assert_once(user_support(n)).
  391.      transf_suppvalue("o",1,B,F,R) :- assert_once(user_support(o)).
  392.      transf_suppvalue("b",U,1,F,R).
  393.      transf_suppvalue("f",U,B,1,R).
  394.      transf_suppvalue("r",U,B,F,1).
  395.  
  396.      var_then_N(N,N) :- !.
  397.      var_then_N(_,_).
  398.  
  399. %%% SET UP SUPPORT STATUS
  400. %%%
  401. %%% set up support environment.
  402. %%% Set proper values in the fields of SP,and DS.
  403.      support_info :-
  404.     support_list_internal(W),
  405.     !,
  406.     support_info_1(W).
  407.  
  408. %%% If user support is given, provide user support information for clauses.
  409.      support_info_1(W) :-
  410.     specified_URsupport(W),
  411.     !, check_unit_clauses_or,
  412.     !, support_info_1_1(W).
  413.      support_info_1(W) :-
  414.     !, support_info_1_1(W).
  415.  
  416.      support_info_1_1(W) :-
  417.     specified_usersupport(W),
  418.     !,
  419.     support_info_2, !.
  420.      support_info_1_1(_) :-
  421.     ubfsupp_1.
  422.  
  423. %%% If user support other than o is specified, but no user support clauses
  424. %%%    are given, then fail.
  425. %%% If user support is o and there is no unit clause, then fail.
  426.      support_info_2 :-
  427.     user_support(o),
  428.     !, check_unit_clauses_or,
  429.     ubfsupp_o, !.
  430.      support_info_2 :-
  431.     check_uorn_support(U),
  432.     ubfsupp(1,U), !.
  433.  
  434.      check_unit_clauses_or :-
  435.     sent_C(cl(_,_,by([_],_,_,_,_))), !.
  436.      check_unit_clauses_or :-
  437.     assert_print_error('No unit clauses !'), !, fail.
  438.  
  439.      check_uorn_support([U|Us]) :-
  440.     user_supportset([U|Us]), !.
  441.      check_uorn_support(_) :-
  442.     assert_print_error('No user support set !'), !, fail.
  443.  
  444.      specified_URsupport([sup(_,_,_,1)|Rs]).
  445.      specified_URsupport([_|Rs]) :-
  446.     !,
  447.     specified_URsupport(Rs).
  448.  
  449.      specified_usersupport([sup(1,_,_,_)|Rs]).
  450.      specified_usersupport([_|Rs]) :-
  451.     !,
  452.     specified_usersupport(Rs).
  453.  
  454. %%% For all unit clauses as user support clauses.
  455.      ubfsupp_o :-
  456.     retract(sent_C(cl(CN1,CSize1,by(Cn1,V11,V12,V1,W1)))),
  457.     ubfsupp_o_1(Cn1,V11,V12,V1,W1,CN1,CSize1),
  458.     fail.
  459.      ubfsupp_o :-
  460.     ubfsupp_1.
  461.  
  462.      ubfsupp_o_1([Ln1],V11,V12,V1,W1,CN1,CSize1) :-
  463.     supplement_clause(1,CN1,CSize1,[Ln1],V11,V12,V1,W1), !.
  464.      ubfsupp_o_1(Cn1,V11,V12,V1,W1,CN1,CSize1) :-
  465.     supplement_clause(0,CN1,CSize1,Cn1,V11,V12,V1,W1), !.
  466.  
  467. %%% Calculate support information, priorities.
  468.      supplement_clause(T,CN1,CSize1,Cn1,V11,V12,V1,W1) :-
  469.     set_sr_status(T,Cn1,CS1,CR1),
  470.     calculate_priority_clause(Cn1,CS1,CR1,CP1),
  471.     list_of_Ns(Cn1,0,F1),
  472.     assertz(sent_c(cl(CSize1,CN1,by(Cn1,V11,V12,V1,W1),
  473.         1,CS1,CR1,0,F1,CP1))). 
  474.  
  475. %%% If the input clause is a user support clause.
  476.      ubfsupp(N,[N|Ns]) :-
  477.     retract(sent_C(cl(CN1,CSize1,by(Cn1,V11,V12,V1,W1)))),
  478.     ubfsupp_neg(CN1,CSize1,Cn1,V11,V12,V1,W1),
  479.     N2 is N + 1, !,
  480.     ubfsupp(N2,Ns).
  481. %%% If the input clause is not a user support clause.
  482.      ubfsupp(N1,[N|Ns]) :-
  483.     retract(sent_C(cl(CN1,CSize1,by(Cn1,V11,V12,V1,W1)))),
  484.     supplement_clause(0,CN1,CSize1,Cn1,V11,V12,V1,W1),
  485.     N2 is N1 + 1, !,
  486.     ubfsupp(N2,[N|Ns]).
  487.      ubfsupp(_,[]) :-
  488.     check_n_support,
  489.     ubfsupp_1.
  490.  
  491. %%% If u is specified as user support.
  492.      ubfsupp_neg(CN1,CSize1,Cn1,V11,V12,V1,W1) :-
  493.     user_support(u),
  494.     supplement_clause(1,CN1,CSize1,Cn1,V11,V12,V1,W1), !.
  495. %%% If n is specified as user support.
  496.      ubfsupp_neg(CN1,CSize1,Cn1,V11,V12,V1,W1) :-
  497.     negclause(Cn1),
  498.     assert_once('neg_clause_with_n_support'),
  499.     supplement_clause(1,CN1,CSize1,Cn1,V11,V12,V1,W1), !.
  500.      ubfsupp_neg(CN1,CSize1,Cn1,V11,V12,V1,W1) :-
  501.     supplement_clause(0,CN1,CSize1,Cn1,V11,V12,V1,W1).
  502.  
  503.      check_n_support :-
  504.     user_support(n),
  505.     !, check_n_support_1, !.
  506.      check_n_support.
  507.  
  508.      check_n_support_1 :-
  509.     neg_clause_with_n_support, !.
  510.      check_n_support_1 :-
  511.     assert_print_error('No negative clauses !'), !, fail.
  512.  
  513. %%% For backward or forward support strategies.
  514.      ubfsupp_1 :-
  515.     ubfsupp_2,
  516.     sentc_to_sentC_z.
  517.  
  518. %%% Take care of one clause at a time.
  519.      ubfsupp_2 :-
  520.     retract(sent_C(cl(CN1,CSize1,by(Cn1,V11,V12,V1,W1)))),
  521.     supplement_clause(1,CN1,CSize1,Cn1,V11,V12,V1,W1),
  522.     !,
  523.     ubfsupp_2.
  524.      ubfsupp_2.
  525.  
  526. %%% Calculate support informations.
  527. %%% The clause is in user support set.
  528.      set_sr_status(1,Cn1,sp(1,1,0),ds(0,0,1)) :-
  529.     negclause(Cn1), !.
  530.      set_sr_status(1,Cn1,sp(1,0,1),ds(0,1,0)) :-
  531.     posclause(Cn1), !.
  532.      set_sr_status(1,Cn1,sp(1,0,0),ds(0,1,1)).
  533. %%% The clause is not in user support set.
  534.      set_sr_status(0,Cn1,sp(0,1,0),ds(X,0,1)) :-
  535.     negclause(Cn1), 
  536.     infinity(X), !.
  537.      set_sr_status(0,Cn1,sp(0,0,1),ds(X,1,0)) :-
  538.     posclause(Cn1), 
  539.     infinity(X), !.
  540.      set_sr_status(0,Cn1,sp(0,0,0),ds(X,1,1)) :-
  541.          infinity(X).
  542.  
  543. %%% Read user_rewrite section.
  544.      read_userrewrite :-
  545.     read(T),
  546.     read_userrewrite(T,E,O),
  547.     assert_rewrite_equiv_list(E),
  548.     assert_rewrite_order_list(O).
  549.      read_userrewrite(end,[],[]).
  550.      read_userrewrite((S->T),E,O) :-
  551.     !,
  552.     assert_rewrite_rule(1,(S->T),_),
  553.     read(T),
  554.     !,
  555.     read_userrewrite(T,E,O).
  556.      read_userrewrite(S1=S2,[S1=S2|E],O) :-
  557.     !,
  558.     read(T),
  559.     !,
  560.     read_userrewrite(T,E,O).
  561.      read_userrewrite(S1>S2,E,[S1>S2|O]) :-
  562.     !,
  563.     read(T),
  564.     !,
  565.     read_userrewrite(T,E,O).
  566.      read_userrewrite(T,_,_) :-
  567.     assert_print_error('Unrecognized expression in user_rewrite section'),
  568.         write_line(15,T),
  569.         !,
  570.     fail.
  571.  
  572. %%% Assert the constant/function/predicate symbol equivalences.
  573.      assert_rewrite_equiv_list([]).
  574.      assert_rewrite_equiv_list([S1=S2|E]) :-
  575.     assert_rewrite_equiv(S1,S2),
  576.     !,
  577.     assert_rewrite_equiv_list(E).
  578.  
  579.      assert_rewrite_equiv(S1,S2) :-
  580.     parse_symbol(S1,S1a,N1),
  581.     parse_symbol(S2,S2a,N2),
  582.     not(rwe([S1a,N1,S2a,N2])),
  583.     !,
  584.         assert_rewrite_equiv_1(S1a,N1,S2a,N2).
  585.      assert_rewrite_equiv(_,_).
  586.  
  587.      assert_rewrite_equiv_1(S1,N1,S2,N2) :-
  588.     not(rwo([S1,N1,S2,N2])),
  589.     not(rwo([S2,N2,S1,N1])),
  590.     !,
  591.     assert(rwe([S1,N1,S2,N2])),
  592.     assert(rwe([S2,N2,S1,N1])),
  593.     bagof1([S3,N3],rwe([S1,N1,S3,N3]),Ss1),
  594.     assert_rewrite_equiv_2(S2,N2,Ss1),
  595.     bagof1([S4,N4],rwe([S4,N4,S2,N2]),Ss2),
  596.     assert_rewrite_equiv_2(S1,N1,Ss2).
  597.      assert_rewrite_equiv_1(_,_,_,_) :-
  598.     assert_print_error('user_rewrite: S1=S2 illegal with S1>S2 or S2>S1'),
  599.     !,
  600.     fail.
  601.  
  602.      assert_rewrite_equiv_2(_,_,[]).
  603.      assert_rewrite_equiv_2(S1,N1,[[S2,N2]|Ss]) :-
  604.     [S1,N1]\==[S2,N2],
  605.     not(rwe([S1,N1,S2,N2])),
  606.     !,
  607.     assert(rwe([S1,N1,S2,N2])),
  608.     assert(rwe([S2,N2,S1,N1])),
  609.     !,
  610.     assert_rewrite_equiv_2(S1,N1,Ss).
  611.      assert_rewrite_equiv_2(S,N,[[_,_]|Ss]) :-
  612.     !,
  613.     assert_rewrite_equiv_2(S,N,Ss).
  614.  
  615.      assert_rewrite_order_list([]).
  616.      assert_rewrite_order_list([S1>S2|E]) :-
  617.     assert_rewrite_order(S1,S2),
  618.     !,
  619.     assert_rewrite_order_list(E).
  620.  
  621. %%% Assert the constant/function/predicate symbol orderings.
  622.      assert_rewrite_order(S1,S2) :-
  623.     parse_symbol(S1,S1a,N1),
  624.     parse_symbol(S2,S2a,N2),
  625.     not(rwo([S1a,N1,S2a,N2])),
  626.     !,
  627.     assert_rewrite_order_1(S1a,N1,S2a,N2).
  628.      assert_rewrite_order(_,_).
  629.  
  630.      assert_rewrite_order_1(S1,N1,S2,N2) :-
  631.     not(rwo([S2,N2,S1,N1])),
  632.         not(rwe([S1,N1,S2,N2])),
  633.     !,
  634.     bagof1([S,N],rwe([S,N,S1,N1]),Ss1a),
  635.     bagof1([S,N],rwo([S,N,S1,N1]),Ss1b),
  636.     append(Ss1a,Ss1b,Ss1),
  637.     bagof1([S,N],rwe([S2,N2,S,N]),Ss2a),
  638.     bagof1([S,N],rwe([S2,N2,S,N]),Ss2b),
  639.     append(Ss2a,Ss2b,Ss2),
  640.     assert_rewrite_order_2([[S1,N1]|Ss1],[[S2,N2]|Ss2]).
  641.      assert_rewrite_order_1(_,_,_,_) :-
  642.     assert_print_error('user_rewrite: S1>S2 illegal with S1=S2 or S2>S1'),
  643.     !,
  644.     fail.
  645.  
  646.      assert_rewrite_order_2([],_).
  647.      assert_rewrite_order_2([[S,N]|Ss1],Ss2) :-
  648.     assert_rewrite_order_3(S,N,Ss2),
  649.     !,
  650.     assert_rewrite_order_2(Ss1,Ss2).
  651.  
  652.      assert_rewrite_order_3(_,_,[]).
  653.      assert_rewrite_order_3(S1,N1,[[S2,N2]|Ss]) :-
  654.     not(rwo([S1,N1,S2,N2])),
  655.     !,
  656.     assert(rwo([S1,N1,S2,N2])),
  657.     !,
  658.     assert_rewrite_order_3(S1,N1,Ss).
  659.      assert_rewrite_order_3(S,N,[[_,_]|Ss]) :-
  660.     !,
  661.     assert_rewrite_order_3(S,N,Ss).
  662.  
  663. %%% Parse a constant/function/predicate symbol into symbol and arity.  
  664. %%% Constants have arity 0.
  665.      parse_symbol(S1,S2,N) :-
  666.     S1=..[S2,N],
  667.     !.
  668.      parse_symbol(S,S,0).
  669.  
  670. %%% Assert and print an error message.
  671.      assert_print_error(X) :-
  672.     assert(error(X)),
  673.     write_line(10,X).
  674.